$\forall$$A$:Type, $I$:MaInterface($A$), $i$:\{$i$:Id$\mid$ ($i$ $\in$ fpf{-}domain($I$))\} . ($I$($i$).2) $\in$ $k$:Knd fp$\rightarrow$ Top